<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Tactics: 更多基本策略</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Tactics<span class="subtitle">更多基本策略</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 本章额外介绍了一些证明策略和手段，
    它们能用来证明更多关于函数式程序的有趣性质。我们会看到：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 如何在“向前证明”和“向后证明”两种风格中使用辅助引理；

</li>
<li> 如何对数据构造子进行论证（特别是，如何利用它们单射且不交的事实）；

</li>
<li> 如何增强归纳假设（以及何时需要增强）；

</li>
<li> 还有通过分类讨论进行论证的更多细节。 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Poly</span>.<br/>
</div>

<div class="doc">
<a name="lab139"></a><h1 class="section"><span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略</h1>

<div class="paragraph"> </div>

 我们经常会遇到待证目标与上下文中的前提或已证引理<b>刚好相同</b>的情况。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">n</span>;<span class="id" type="var">o</span>] = [<span class="id" type="var">n</span>;<span class="id" type="var">p</span>] →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">n</span>;<span class="id" type="var">o</span>] = [<span class="id" type="var">m</span>;<span class="id" type="var">p</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span> <span class="id" type="var">eq<sub>1</sub></span> <span class="id" type="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">eq<sub>1</sub></span>.<br/>
</div>

<div class="doc">
我们可以像之前那样用“<span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">eq<sub>2</sub></span>.</span>  <span class="inlinecode"><span class="id" type="tactic">reflexivity</span>.</span>”来完成。
    不过如果我们使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略，只需一步就能达到同样的效果： 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>2</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略也可以配合<b>条件（Conditional）</b>假设和引理来使用：
    如果被应用的语句是一个蕴含式，那么该蕴含式的前提就会被添加到待证子目标列表中。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly2</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">q</span> <span class="id" type="var">r</span> : <span class="id" type="var">nat</span>), <span class="id" type="var">q</span> = <span class="id" type="var">r</span> → [<span class="id" type="var">q</span>;<span class="id" type="var">o</span>] = [<span class="id" type="var">r</span>;<span class="id" type="var">p</span>]) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">n</span>;<span class="id" type="var">o</span>] = [<span class="id" type="var">m</span>;<span class="id" type="var">p</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span> <span class="id" type="var">eq<sub>1</sub></span> <span class="id" type="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>2</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>1</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
通常，当我们使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> 时，语句 <span class="inlinecode"><span class="id" type="var">H</span></span> 会以一个绑定了某些
    <b>通用变量（Universal Variables）</b> 的 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> 开始。在 Coq 针对 <span class="inlinecode"><span class="id" type="var">H</span></span>
    的结论匹配当前目标时，它会尝试为这些变量查找适当的值。例如，
    当我们在以下证明中执行 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">eq<sub>2</sub></span></span> 时，<span class="inlinecode"><span class="id" type="var">eq<sub>2</sub></span></span> 中的通用变量 <span class="inlinecode"><span class="id" type="var">q</span></span>
    会以 <span class="inlinecode"><span class="id" type="var">n</span></span> 实例化，而 <span class="inlinecode"><span class="id" type="var">r</span></span> 会以 <span class="inlinecode"><span class="id" type="var">m</span></span> 实例化。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly2a</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">n</span>,<span class="id" type="var">n</span>) = (<span class="id" type="var">m</span>,<span class="id" type="var">m</span>)  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">q</span> <span class="id" type="var">r</span> : <span class="id" type="var">nat</span>), (<span class="id" type="var">q</span>,<span class="id" type="var">q</span>) = (<span class="id" type="var">r</span>,<span class="id" type="var">r</span>) → [<span class="id" type="var">q</span>] = [<span class="id" type="var">r</span>]) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">n</span>] = [<span class="id" type="var">m</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">eq<sub>1</sub></span> <span class="id" type="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>2</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>1</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab140"></a><h4 class="section">练习：2 星, standard, optional (silly_ex)</h4>
 请完成以下证明，不要使用 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly_ex</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">evenb</span> <span class="id" type="var">n</span> = <span class="id" type="var">true</span> → <span class="id" type="var">oddb</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) = <span class="id" type="var">true</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">oddb</span> 3 = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">evenb</span> 4 = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 要使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略，被应用的事实（的结论）必须精确地匹配证明目标：
    例如, 当等式的左右两边互换后，<span class="inlinecode"><span class="id" type="tactic">apply</span></span> 就无法起效了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly3_firsttry</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">true</span> = (<span class="id" type="var">n</span> =? 5)  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) =? 7 = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">H</span>.<br/>
</div>

<div class="doc">
在这里，我们无法直接使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span>，不过我们可以用 <span class="inlinecode"><span class="id" type="tactic">symmetry</span></span> 策略
    它会交换证明目标中等式的左右两边。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">symmetry</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. </div>

<div class="doc">
（此处的 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 是可选的，因为 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 会在需要时先进行化简。） 
</div>
<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab141"></a><h4 class="section">练习：3 星, standard (apply_exercise1)</h4>
 （<b>提示</b>：你可以配合之前定义的引理来使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span>，不仅限于当前上下文中的前提。
    记住 <span class="inlinecode"><span class="id" type="var">Search</span></span> 是你的朋友。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">rev_exercise1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l</span> <span class="id" type="var">l'</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">l</span> = <span class="id" type="var">rev</span> <span class="id" type="var">l'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">l'</span> = <span class="id" type="var">rev</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab142"></a><h4 class="section">练习：1 星, standard, optional (apply_rewrite)</h4>
 简述 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 与 <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> 策略之区别。哪些情况下二者均可有效利用？ 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab143"></a><h1 class="section"><span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> 策略</h1>

<div class="paragraph"> </div>

 以下愚蠢的例子在一行中使用了两次改写来将 <span class="inlinecode">[<span class="id" type="var">a</span>;<span class="id" type="var">b</span>]</span> 变成 <span class="inlinecode">[<span class="id" type="var">e</span>;<span class="id" type="var">f</span>]</span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">trans_eq_example</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">d</span> <span class="id" type="var">e</span> <span class="id" type="var">f</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">a</span>;<span class="id" type="var">b</span>] = [<span class="id" type="var">c</span>;<span class="id" type="var">d</span>] →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">c</span>;<span class="id" type="var">d</span>] = [<span class="id" type="var">e</span>;<span class="id" type="var">f</span>] →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">a</span>;<span class="id" type="var">b</span>] = [<span class="id" type="var">e</span>;<span class="id" type="var">f</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">d</span> <span class="id" type="var">e</span> <span class="id" type="var">f</span> <span class="id" type="var">eq<sub>1</sub></span> <span class="id" type="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> → <span class="id" type="var">eq<sub>1</sub></span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">eq<sub>2</sub></span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
由于这种模式十分常见，因此我们希望一劳永逸地把它作为一条引理记录下来，
    即等式具有传递性。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">trans_eq</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) (<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> : <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span> → <span class="id" type="var">m</span> = <span class="id" type="var">o</span> → <span class="id" type="var">n</span> = <span class="id" type="var">o</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">X</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">eq<sub>1</sub></span> <span class="id" type="var">eq<sub>2</sub></span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">eq<sub>1</sub></span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
现在，按理说我们应该可以用 <span class="inlinecode"><span class="id" type="var">trans_eq</span></span> 来证明前面的例子了。
    然而，为此我们还需要稍微改进一下 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">trans_eq_example'</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">d</span> <span class="id" type="var">e</span> <span class="id" type="var">f</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">a</span>;<span class="id" type="var">b</span>] = [<span class="id" type="var">c</span>;<span class="id" type="var">d</span>] →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">c</span>;<span class="id" type="var">d</span>] = [<span class="id" type="var">e</span>;<span class="id" type="var">f</span>] →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">a</span>;<span class="id" type="var">b</span>] = [<span class="id" type="var">e</span>;<span class="id" type="var">f</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">d</span> <span class="id" type="var">e</span> <span class="id" type="var">f</span> <span class="id" type="var">eq<sub>1</sub></span> <span class="id" type="var">eq<sub>2</sub></span>.<br/>
</div>

<div class="doc">
如果此时我们只是告诉 Coq <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">trans_eq</span></span>，那么它会
    （根据该引理的结论对证明目标的匹配）说 <span class="inlinecode"><span class="id" type="var">X</span></span> 应当实例化为 <span class="inlinecode">[<span class="id" type="var">nat</span>]</span>、<span class="inlinecode"><span class="id" type="var">n</span></span>
    实例化为 <span class="inlinecode">[<span class="id" type="var">a</span>,<span class="id" type="var">b</span>]</span>、以及 <span class="inlinecode"><span class="id" type="var">o</span></span> 实例化为 <span class="inlinecode">[<span class="id" type="var">e</span>,<span class="id" type="var">f</span>]</span>。然而，匹配过程并没有为
    <span class="inlinecode"><span class="id" type="var">m</span></span> 确定实例：我们必须在 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 的调用后面加上 <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode">(<span class="id" type="var">m</span>:=[<span class="id" type="var">c</span>,<span class="id" type="var">d</span>])</span>
    来显式地提供一个实例。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">trans_eq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">m</span>:=[<span class="id" type="var">c</span>;<span class="id" type="var">d</span>]).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>1</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">eq<sub>2</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
实际上，我们通常不必在 <span class="inlinecode"><span class="id" type="keyword">with</span></span> 从句中包含名字 <span class="inlinecode"><span class="id" type="var">m</span></span>，Coq
    一般足够聪明来确定我们给出的实例。我们也可以写成：
    <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">trans_eq</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode">[<span class="id" type="var">c</span>;<span class="id" type="var">d</span>]</span>。 
<div class="paragraph"> </div>

<a name="lab144"></a><h4 class="section">练习：3 星, standard, optional (apply_with_exercise)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">trans_eq_exercise</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">m</span> = (<span class="id" type="var">minustwo</span> <span class="id" type="var">o</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">n</span> + <span class="id" type="var">p</span>) = <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">n</span> + <span class="id" type="var">p</span>) = (<span class="id" type="var">minustwo</span> <span class="id" type="var">o</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab145"></a><h1 class="section">The <span class="inlinecode"><span class="id" type="tactic">injection</span></span> and <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> Tactics</h1>

<div class="paragraph"> </div>

 回想自然数的定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">nat</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">O</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">S</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="var">nat</span>.
<div class="paragraph"> </div>

</div>
    我们可从该定义中观察到，所有的数都是两种形式之一：要么是构造子 <span class="inlinecode"><span class="id" type="var">O</span></span>，
    要么就是将构造子 <span class="inlinecode"><span class="id" type="var">S</span></span> 应用到另一个数上。不过这里还有无法直接看到的：
    自然数的定义（以及我们对其它编程语言中数据类型声明的工作方式的非形式化理解）
    中还蕴含了两个事实：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 构造子 <span class="inlinecode"><span class="id" type="var">S</span></span> 是<b>单射（Injective）</b>的。
      即，如果 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>，那么 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 必定成立。

<div class="paragraph"> </div>


</li>
<li> 构造子 <span class="inlinecode"><span class="id" type="var">O</span></span> 和 <span class="inlinecode"><span class="id" type="var">S</span></span> 是<b>不相交（Disjoint）</b>的。
      即，对于任何 <span class="inlinecode"><span class="id" type="var">n</span></span>，<span class="inlinecode"><span class="id" type="var">O</span></span> 都不等于 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>。

</li>
</ul>
    类似的原理同样适用于所有归纳定义的类型：所有构造子都是单射的，
    而不同构造子构造出的值绝不可能相等。对于列表来说，<span class="inlinecode"><span class="id" type="var">cons</span></span> 构造子是单射的，
    而 <span class="inlinecode"><span class="id" type="var">nil</span></span> 不同于任何非空列表。对于布尔值来说，<span class="inlinecode"><span class="id" type="var">true</span></span> 和 <span class="inlinecode"><span class="id" type="var">false</span></span> 是不同的。
    因为 <span class="inlinecode"><span class="id" type="var">true</span></span> 和 <span class="inlinecode"><span class="id" type="var">false</span></span> 二者都不接受任何参数，它们的单射性并不有趣。
    其它归纳类型亦是如此。 
<div class="paragraph"> </div>

 例如，我们可以使用定义在 <span class="inlinecode"><span class="id" type="var">Basics.v</span></span> 中的 <span class="inlinecode"><span class="id" type="var">pred</span></span> 函数来证明 <span class="inlinecode"><span class="id" type="var">S</span></span> 的单射性。
. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">S_injective</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> = <span class="id" type="var">S</span> <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H<sub>2</sub></span>: <span class="id" type="var">n</span> = <span class="id" type="var">pred</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)). { <span class="id" type="tactic">reflexivity</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
    这个技巧可以通过编写构造子的等价的 <span class="inlinecode"><span class="id" type="var">pred</span></span> 来推广到任意的构造子上 ——
    即编写一个 “撤销” 一次构造子调用的函数。
    作为一种更加简便的替代品， Coq提供了叫做 <span class="inlinecode"><span class="id" type="tactic">injection</span></span> 的策略来让我们利用任意构造子的单射性。
    此处是使用 <span class="inlinecode"><span class="id" type="tactic">injection</span></span> 对上面定理的另一种证法。

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">S_injective'</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> = <span class="id" type="var">S</span> <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">H</span>.<br/>
</div>

<div class="doc">
通过在此处编写 <span class="inlinecode"><span class="id" type="tactic">injection</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> ，
    我们命令Coq使用构造子的单射性来产生所有它能从 <span class="inlinecode"><span class="id" type="var">H</span></span> 所推出的等式。
    每一个产生的等式都作为一个前件附加在目标上。
    在这个例子中，附加了前件 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 。

</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">Hnm</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Hnm</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
此处展示了一个 <span class="inlinecode"><span class="id" type="tactic">injection</span></span> 如何直接得出多个等式的有趣例子。

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">injection_ex<sub>1</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>; <span class="id" type="var">m</span>] = [<span class="id" type="var">o</span>; <span class="id" type="var">o</span>] →<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>] = [<span class="id" type="var">m</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H<sub>1</sub></span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">injection</span></span> 的 "<span class="inlinecode"><span class="id" type="keyword">as</span></span>" 变体允许我们而非Coq来为引入的等式选择名称。

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">injection_ex<sub>2</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>] = [<span class="id" type="var">m</span>] →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> <span class="id" type="var">Hnm</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hnm</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab146"></a><h4 class="section">练习：1 星, standard (injection_ex<sub>3</sub>)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">injection_ex<sub>3</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">l</span> <span class="id" type="var">j</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">x</span> :: <span class="id" type="var">y</span> :: <span class="id" type="var">l</span> = <span class="id" type="var">z</span> :: <span class="id" type="var">j</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">y</span> :: <span class="id" type="var">l</span> = <span class="id" type="var">x</span> :: <span class="id" type="var">j</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">x</span> = <span class="id" type="var">y</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 So much for injectivity of constructors.  What about disjointness?

<div class="paragraph"> </div>

    The principle of disjointness says that two terms beginning with
    different constructors (like <span class="inlinecode"><span class="id" type="var">O</span></span> and <span class="inlinecode"><span class="id" type="var">S</span></span>, or <span class="inlinecode"><span class="id" type="var">true</span></span> and <span class="inlinecode"><span class="id" type="var">false</span></span>)
    can never be equal.  This means that, any time we find ourselves
    working in a context where we've _assumed_ that two such terms are
    equal, we are justified in concluding anything we want to (because
    the assumption is nonsensical).

<div class="paragraph"> </div>

    The <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> tactic embodies this principle: It is used on a
    hypothesis involving an equality between different
    constructors (e.g., <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">O</span></span>), and it solves the current goal
    immediately.  For example: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqb_0_l</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;&nbsp;0 =? <span class="id" type="var">n</span> = <span class="id" type="var">true</span> → <span class="id" type="var">n</span> = 0.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>.<br/>
</div>

<div class="doc">
我们可以通过对 <span class="inlinecode"><span class="id" type="var">n</span></span> 进行分类讨论来继续。第一种分类是平凡的。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
</div>

<div class="doc">
However, the second one doesn't look so simple: assuming <span class="inlinecode">0</span>
    <span class="inlinecode">=?</span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>, we must show <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>!  The way forward is to
    observe that the assumption itself is nonsensical: 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
    如果我们对这个假设使用 <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> ，
    Coq便会确认我们当前正在证明的目标不可行，并同时移除它，不再考虑。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
本例是逻辑学原理<b>爆炸原理</b>的一个实例，它断言矛盾的前提会推出任何东西，
    甚至是假命题！ 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">discriminate_ex<sub>1</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> = <span class="id" type="var">O</span> →<br/>
&nbsp;&nbsp;2 + 2 = 5.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">contra</span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">contra</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">discriminate_ex<sub>2</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">false</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>] = [<span class="id" type="var">m</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">contra</span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">contra</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
爆炸原理可能令你费解，那么请记住上述证明并不肯定其后件，
    而是说明：倘若荒谬的前件成立，则会得出荒谬的结论。
    下一章将进一步讨论爆炸原理。 
<div class="paragraph"> </div>

<a name="lab147"></a><h4 class="section">练习：1 星, standard (discriminate_ex<sub>3</sub>)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">discriminate_ex<sub>3</sub></span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">l</span> <span class="id" type="var">j</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span> :: <span class="id" type="var">y</span> :: <span class="id" type="var">l</span> = [] →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span> = <span class="id" type="var">z</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 构造子的单射性允许我们论证 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode">(<span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span>),</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>。
    此蕴含式的交流（converse）是一个更加一般的关于构造子和函数的事实的实例，
    在后面的几个地方我们会发现它很方便： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">f_equal</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">A</span> <span class="id" type="var">B</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">f</span>: <span class="id" type="var">A</span> → <span class="id" type="var">B</span>) (<span class="id" type="var">x</span> <span class="id" type="var">y</span>: <span class="id" type="var">A</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">x</span> = <span class="id" type="var">y</span> → <span class="id" type="var">f</span> <span class="id" type="var">x</span> = <span class="id" type="var">f</span> <span class="id" type="var">y</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">A</span> <span class="id" type="var">B</span> <span class="id" type="var">f</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab148"></a><h1 class="section">对前提使用策略</h1>

<div class="paragraph"> </div>

 默认情况下，大部分策略会作用于目标公式并保持上下文不变。然而，
    大部分策略还有对应的变体来对上下文中的语句执行类似的操作。

<div class="paragraph"> </div>

    例如，策略 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> 会对上下文中名为 <span class="inlinecode"><span class="id" type="var">H</span></span> 的前提执行化简。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">S_inj</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">b</span> : <span class="id" type="var">bool</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">S</span> <span class="id" type="var">n</span>) =? (<span class="id" type="var">S</span> <span class="id" type="var">m</span>) = <span class="id" type="var">b</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> =? <span class="id" type="var">m</span> = <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">b</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
类似地，<span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">L</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> 会针对上下文中的前提 <span class="inlinecode"><span class="id" type="var">H</span></span> 匹配某些
    （形如 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> 中的）条件语句 <span class="inlinecode"><span class="id" type="var">L</span></span>。然而，与一般的 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 不同
    （它将匹配 <span class="inlinecode"><span class="id" type="var">Y</span></span> 的目标改写为子目标 <span class="inlinecode"><span class="id" type="var">X</span></span>），<span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">L</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> 会针对
    <span class="inlinecode"><span class="id" type="var">X</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">H</span></span>，如果成功，就将其替换为 <span class="inlinecode"><span class="id" type="var">Y</span></span>。

<div class="paragraph"> </div>

    换言之，<span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">L</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> 给了我们一种“正向推理”的方式：根据 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Y</span></span>
    和一个匹配 <span class="inlinecode"><span class="id" type="var">X</span></span> 的前提，它会产生一个匹配 <span class="inlinecode"><span class="id" type="var">Y</span></span> 的前提。作为对比，<span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">L</span></span>
    是一种“反向推理”：它表示如果我们知道 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> 并且试图证明 <span class="inlinecode"><span class="id" type="var">Y</span></span>，
    那么证明 <span class="inlinecode"><span class="id" type="var">X</span></span> 就足够了。

<div class="paragraph"> </div>

    下面是前面证明的一种变体，它始终使用正向推理而非反向推理。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly3'</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">n</span> =? 5 = <span class="id" type="var">true</span> → (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) =? 7 = <span class="id" type="var">true</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">true</span> = (<span class="id" type="var">n</span> =? 5)  →<br/>
&nbsp;&nbsp;<span class="id" type="var">true</span> = ((<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) =? 7).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">eq</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">symmetry</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">eq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">symmetry</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
正向推理从<b>给定</b>的东西开始（即前提、已证明的定理），
    根据它们迭代地刻画结论直到抵达目标。反向推理从<b>目标</b>开始，
    迭代地推理蕴含目标的东西，直到抵达前提或已证明的定理。

<div class="paragraph"> </div>

    如果你之前见过非形式化的证明（例如在数学或计算机科学课上），
    它们使用的应该是正向推理。通常，Coq 习惯上倾向于使用反向推理，
    但在某些情况下，正向推理更易于思考。 
<div class="paragraph"> </div>

<a name="lab149"></a><h4 class="section">练习：3 星, standard, recommended (plus_n_n_injective)</h4>
 请在此证明中练习使用“in”形式的变体。（提示：使用 <span class="inlinecode"><span class="id" type="var">plus_n_Sm</span></span>。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_n_n_injective</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> + <span class="id" type="var">n</span> = <span class="id" type="var">m</span> + <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab150"></a><h1 class="section">变换归纳法则</h1>

<div class="paragraph"> </div>

 在 Coq 中进行归纳证明时，有时控制归纳假设的确切形式是十分重要的。
    特别是，在调用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略前，我们用 <span class="inlinecode"><span class="id" type="tactic">intros</span></span>
    将假设从目标移到上下文中时要十分小心。例如，假设我们要证明 <span class="inlinecode"><span class="id" type="var">double</span></span>
    函数式单射的 &mdash; 即，它将不同的参数映射到不同的结果：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Theorem</span>&nbsp;<span class="id" type="var">double_injective</span>:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;<span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">double</span>&nbsp;<span class="id" type="var">n</span>&nbsp;=&nbsp;<span class="id" type="var">double</span>&nbsp;<span class="id" type="var">m</span>&nbsp;→&nbsp;<span class="id" type="var">n</span>&nbsp;=&nbsp;<span class="id" type="var">m</span>.
<div class="paragraph"> </div>

</div>
    其证明的<b>开始方式</b>有点微妙：如果我们以

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>&nbsp;<span class="id" type="var">n</span>. <span class="id" type="tactic">induction</span>&nbsp;<span class="id" type="var">n</span>.
<div class="paragraph"> </div>

</div>
    开始，那么一切都好。然而假如以

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">m</span>. <span class="id" type="tactic">induction</span>&nbsp;<span class="id" type="var">n</span>.
<div class="paragraph"> </div>

</div>
    开始，就会卡在归纳情况中... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">double_injective_FAILED</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">double</span> <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">intros</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="tactic">f_equal</span>.<br/>
</div>

<div class="doc">
此时，归纳假设 <span class="inlinecode"><span class="id" type="var">IHn'</span></span> <b>不会</b>给出 <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m'</span></span> &mdash; 会有个额外的 <span class="inlinecode"><span class="id" type="var">S</span></span> 阻碍 &mdash;
    因此该目标无法证明。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
哪里出了问题？ 
<div class="paragraph"> </div>

 问题在于，我们在调用归纳假设的地方已经将 <span class="inlinecode"><span class="id" type="var">m</span></span> 引入了上下文中 &mdash;
    直观上，我们已经告诉了 Coq“我们来考虑具体的 <span class="inlinecode"><span class="id" type="var">n</span></span> 和 <span class="inlinecode"><span class="id" type="var">m</span></span>...”，
    而现在必须为这些<b>具体的</b> <span class="inlinecode"><span class="id" type="var">n</span></span> 和 <span class="inlinecode"><span class="id" type="var">m</span></span> 证明 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>，
    然后才有 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>。

<div class="paragraph"> </div>

    下一个策略 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 告诉 Coq：我们要对 <span class="inlinecode"><span class="id" type="var">n</span></span> 归纳来证明该目标。
    也就是说，我们要证明对于<b>所有的</b> <span class="inlinecode"><span class="id" type="var">n</span></span>，命题

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> = "if <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>, then <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>"

</li>
</ul>

<div class="paragraph"> </div>

    成立，需通过证明

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">O</span></span>

<div class="paragraph"> </div>

        （即，若“<span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">O</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 则 <span class="inlinecode"><span class="id" type="var">O</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>”）和

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>

<div class="paragraph"> </div>

        （即，若“<span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 则 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>”蕴含“若
        <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 则 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>”）来得出。

</li>
</ul>

<div class="paragraph"> </div>

    如果我们仔细观察第二个语句，就会发现它说了奇怪的事情：即，对于一个<b>具体的</b>
    <span class="inlinecode"><span class="id" type="var">m</span></span>，如果我们知道

<div class="paragraph"> </div>

<ul class="doclist">
<li> “若 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 则 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>”

</li>
</ul>

<div class="paragraph"> </div>

    那么我们就能证明

<div class="paragraph"> </div>

<ul class="doclist">
<li> “若 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 则 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>”。

</li>
</ul>

<div class="paragraph"> </div>

    要理解为什么它很奇怪，我们来考虑一个具体的 <span class="inlinecode"><span class="id" type="var">m</span></span> &mdash;
    比如说，<span class="inlinecode">5</span>。该语句就会这样说：如果我们知道

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">Q</span></span> = “若 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">10</span> 则 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">5</span>”

</li>
</ul>

<div class="paragraph"> </div>

    那么我们就能证明

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> = “若 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">10</span> 则 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">5</span>”。

</li>
</ul>

<div class="paragraph"> </div>

    但是知道 <span class="inlinecode"><span class="id" type="var">Q</span></span> 对于证明 <span class="inlinecode"><span class="id" type="var">R</span></span> 来说并没有任何帮助！（如果我们试着根据 <span class="inlinecode"><span class="id" type="var">Q</span></span>
    证明 <span class="inlinecode"><span class="id" type="var">R</span></span> from <span class="inlinecode"><span class="id" type="var">Q</span></span>，就会以“假设 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">10</span>..”这样的句子开始，
    不过之后我们就会卡住：知道 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 为 <span class="inlinecode">10</span> 并不能告诉我们
    <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 是否为 <span class="inlinecode">10</span>，因此 <span class="inlinecode"><span class="id" type="var">Q</span></span> 是没有用的。） 
<div class="paragraph"> </div>

 当 <span class="inlinecode"><span class="id" type="var">m</span></span> 已经在上下文中时，试图对 <span class="inlinecode"><span class="id" type="var">n</span></span> 进行归纳来进行此证明是行不通的，
    因为我们之后要尝试证明涉及<b>每一个</b> <span class="inlinecode"><span class="id" type="var">n</span></span> 的命题，而不只是<b>单个</b> <span class="inlinecode"><span class="id" type="var">m</span></span>。 
<div class="paragraph"> </div>

 对 <span class="inlinecode"><span class="id" type="var">double_injective</span></span> 的成功证明将 <span class="inlinecode"><span class="id" type="var">m</span></span> 留在了目标语句中 <span class="inlinecode"><span class="id" type="tactic">induction</span></span>
    作用于 <span class="inlinecode"><span class="id" type="var">n</span></span> 的地方：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">double_injective</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">double</span> <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">m</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
注意，此时的证明目标和归纳假设是不同的：证明目标要求我们证明更一般的事情
    （即，为<b>每一个</b> <span class="inlinecode"><span class="id" type="var">m</span></span> 证明该语句），而归纳假设 <span class="inlinecode"><span class="id" type="var">IH</span></span> 相应地更加灵活，
    允许我们在应用归纳假设时选择任何想要的 <span class="inlinecode"><span class="id" type="var">m</span></span>。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">m</span> <span class="id" type="var">eq</span>.<br/>
</div>

<div class="doc">
现在我们选择了一个具体的 <span class="inlinecode"><span class="id" type="var">m</span></span> 并引入了假设 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>。
    由于我们对 <span class="inlinecode"><span class="id" type="var">n</span></span> 做了情况分析，因此还要对 <span class="inlinecode"><span class="id" type="var">m</span></span> 做情况分析来保持两边“同步”。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
0 的情况很显然： 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="tactic">f_equal</span>.<br/>
</div>

<div class="doc">
到这里，由于我们在 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 的第二个分支中，因此上下文中涉及到的 <span class="inlinecode"><span class="id" type="var">m'</span></span>
    就是我们开始讨论的 <span class="inlinecode"><span class="id" type="var">m</span></span> 的前趋。由于我们也在归纳的 <span class="inlinecode"><span class="id" type="var">S</span></span> 分支中，这就很完美了：
    如果我们在归纳假设中用当前的 <span class="inlinecode"><span class="id" type="var">m'</span></span>（此实例由下一步的 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 自动产生）
    实例化一般的 <span class="inlinecode"><span class="id" type="var">m</span></span>，那么 <span class="inlinecode"><span class="id" type="var">IHn'</span></span> 就刚好能给出我们需要的来结束此证明。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHn'</span>. <span class="id" type="tactic">injection</span> <span class="id" type="var">eq</span> <span class="id" type="keyword">as</span> <span class="id" type="var">goal</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">goal</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
What you should take away from all this is that we need to be
    careful, when using induction, that we are not trying to prove
    something too specific: To prove a property of <span class="inlinecode"><span class="id" type="var">n</span></span> and <span class="inlinecode"><span class="id" type="var">m</span></span> by
    induction on <span class="inlinecode"><span class="id" type="var">n</span></span>, it is sometimes important to leave <span class="inlinecode"><span class="id" type="var">m</span></span>
    generic. 
<div class="paragraph"> </div>

 以下练习需要同样的模式。 
<div class="paragraph"> </div>

<a name="lab151"></a><h4 class="section">练习：2 星, standard (eqb_true)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqb_true</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> =? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> → <span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab152"></a><h4 class="section">练习：2 星, advanced (eqb_true_informal)</h4>
 给出一个详细的 <span class="inlinecode"><span class="id" type="var">eqb_true</span></span> 的非形式化证明，量词要尽可能明确。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_informal_proof</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 在 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 之前做一些 <span class="inlinecode"><span class="id" type="tactic">intros</span></span> 来获得更一般归纳假设并不总是奏效。
    有时需要对量化的变量做一下<b>重排</b>。例如，假设我们想要通过对 <span class="inlinecode"><span class="id" type="var">m</span></span>
    而非 <span class="inlinecode"><span class="id" type="var">n</span></span> 进行归纳来证明 <span class="inlinecode"><span class="id" type="var">double_injective</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">double_injective_take2_FAILED</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">double</span> <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" type="tactic">intros</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="tactic">f_equal</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;和前面一样，又卡在这儿了。&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
问题在于，要对 <span class="inlinecode"><span class="id" type="var">m</span></span> 进行归纳，我们首先必须对 <span class="inlinecode"><span class="id" type="var">n</span></span> 归纳。
    （如果我们不引入任何东西就执行 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>，Coq 就会自动为我们引入 <span class="inlinecode"><span class="id" type="var">n</span></span>！） 
<div class="paragraph"> </div>

 我们可以对它做什么？一种可能就是改写该引理的陈述使得 <span class="inlinecode"><span class="id" type="var">m</span></span> 在 <span class="inlinecode"><span class="id" type="var">n</span></span> 之前量化。
    这样是可行的，不过它不够好：我们不想调整该引理的陈述来适应具体的证明策略！
    我们更想以最清晰自然的方式陈述它。 
<div class="paragraph"> </div>

 我们可以先引入所有量化的变量，然后<b>重新一般化（re-generalize）</b>
    其中的一个或几个，选择性地从上下文中挑出几个变量并将它们放回证明目标的开始处。
    用 <span class="inlinecode"><span class="id" type="tactic">generalize</span></span> <span class="inlinecode"><span class="id" type="tactic">dependent</span></span> 策略就能做到。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">double_injective_take2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">double</span> <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">m</span></span>&nbsp;are&nbsp;both&nbsp;in&nbsp;the&nbsp;context&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">n</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;现在&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;回到了目标中，我们可以对&nbsp;<span class="inlinecode"><span class="id" type="var">m</span></span>&nbsp;进行归纳并得到足够一般的归纳假设了。&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>] <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="tactic">f_equal</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHm'</span>. <span class="id" type="tactic">injection</span> <span class="id" type="var">eq</span> <span class="id" type="keyword">as</span> <span class="id" type="var">goal</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">goal</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
我们来看一下此定理的非形式化证明。注意我们保持 <span class="inlinecode"><span class="id" type="var">n</span></span>
    的量化状态并通过归纳证明的命题，对应于我们形式化证明中依赖的一般化。

<div class="paragraph"> </div>

    <b>定理</b>：对于任何自然数 <span class="inlinecode"><span class="id" type="var">n</span></span> 和 <span class="inlinecode"><span class="id" type="var">m</span></span>，若 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>，则 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>。

<div class="paragraph"> </div>

    <b>证明</b>：令 <span class="inlinecode"><span class="id" type="var">m</span></span> 为一个 <span class="inlinecode"><span class="id" type="var">nat</span></span>。我们通过对 <span class="inlinecode"><span class="id" type="var">m</span></span> 进行归纳来证明，对于任何 <span class="inlinecode"><span class="id" type="var">n</span></span>，
        若 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>，则 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 首先，设 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>，而 <span class="inlinecode"><span class="id" type="var">n</span></span> 是一个数使得 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>。
        我们必须证明 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>。

<div class="paragraph"> </div>

        由于 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>，根据 <span class="inlinecode"><span class="id" type="var">double</span></span> 的定义，我们有 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>。此时对于 <span class="inlinecode"><span class="id" type="var">n</span></span>
        需要考虑两种情况。若 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>，则得证，因为 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span>，正如所需。
        否则，若对于某个 <span class="inlinecode"><span class="id" type="var">n'</span></span> 有 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>，我们就会导出矛盾：根据 <span class="inlinecode"><span class="id" type="var">double</span></span>
        的定义，我们可得出 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>))</span>，但它与 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>
        相矛盾。

<div class="paragraph"> </div>


</li>
<li> 其次，设 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span>，而 <span class="inlinecode"><span class="id" type="var">n</span></span> 同样是一个数使得 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>。
        我们必须证明 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span>，根据归纳假设，对于任何数 <span class="inlinecode"><span class="id" type="var">s</span></span>，若
        <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span>，则 <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m'</span></span>。

<div class="paragraph"> </div>

        根据 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span> 的事实以及 <span class="inlinecode"><span class="id" type="var">double</span></span> 的定义我们有 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m'</span>))</span>。
        此时对于 <span class="inlinecode"><span class="id" type="var">n</span></span> 需要考虑两种情况。

<div class="paragraph"> </div>

        若 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>，则根据 <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> 的定义会得出矛盾。

<div class="paragraph"> </div>

        因此，我们假设对于某个 <span class="inlinecode"><span class="id" type="var">n'</span></span>，有 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>，同样根据 <span class="inlinecode"><span class="id" type="var">double</span></span>
        的定义，我们有 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>))</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m'</span>))</span>，它可通过反演
        <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span> 得出。以 <span class="inlinecode"><span class="id" type="var">n'</span></span> 实例化归纳假设允许我们得出
        <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m'</span></span> 的结论，显然 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span>。因此 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> 且 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">m'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>，
        此即我们所欲证。 <span class="proofbox">&#9744;</span> 
</li>
</ul>

<div class="paragraph"> </div>

 在结束本节去做习题之前，我们先稍微跑个题，使用 <span class="inlinecode"><span class="id" type="var">eqb_true</span></span>
    来证明一个标识符的类似性质以备后用： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqb_id_true</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">y</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">eqb_id</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> = <span class="id" type="var">true</span> → <span class="id" type="var">x</span> = <span class="id" type="var">y</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> [<span class="id" type="var">m</span>] [<span class="id" type="var">n</span>]. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H'</span> : <span class="id" type="var">m</span> = <span class="id" type="var">n</span>). { <span class="id" type="tactic">apply</span> <span class="id" type="var">eqb_true</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H'</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab153"></a><h4 class="section">练习：3 星, standard, recommended (gen_dep_practice)</h4>
 通过对 <span class="inlinecode"><span class="id" type="var">l</span></span> 进行归纳来证明它。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">nth_error_after_last</span>: <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">length</span> <span class="id" type="var">l</span> = <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">nth_error</span> <span class="id" type="var">l</span> <span class="id" type="var">n</span> = <span class="id" type="var">None</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab154"></a><h1 class="section">展开定义</h1>

<div class="paragraph"> </div>

 It sometimes happens that we need to manually unfold a name that
    has been introduced by a <span class="inlinecode"><span class="id" type="keyword">Definition</span></span> so that we can manipulate
    its right-hand side.  For example, if we define... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">square</span> <span class="id" type="var">n</span> := <span class="id" type="var">n</span> * <span class="id" type="var">n</span>.<br/>
</div>

<div class="doc">
...并试图证明一个关于 <span class="inlinecode"><span class="id" type="var">square</span></span> 的简单事实... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">square_mult</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">square</span> (<span class="id" type="var">n</span> * <span class="id" type="var">m</span>) = <span class="id" type="var">square</span> <span class="id" type="var">n</span> * <span class="id" type="var">square</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
...那么就会卡住：此时 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 无法化简任何东西，而由于我们尚未证明任何关于
    <span class="inlinecode"><span class="id" type="var">square</span></span> 的事实，也就没有任何可以用来 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 或 <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> 的东西。

<div class="paragraph"> </div>

    为此，我们可以手动用 <span class="inlinecode"><span class="id" type="tactic">unfold</span></span> 展开 <span class="inlinecode"><span class="id" type="var">square</span></span> 的定义： 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">square</span>.<br/>
</div>

<div class="doc">
现在我们有很多工作要做：等式两边都是涉及乘法的表达式，
    而我们有很多可用的关于乘法的事实。特别是，我们知道它满足交换性和结合性，
    该引理据此不难证明。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">mult_assoc</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H</span> : <span class="id" type="var">n</span> * <span class="id" type="var">m</span> * <span class="id" type="var">n</span> = <span class="id" type="var">n</span> * <span class="id" type="var">n</span> * <span class="id" type="var">m</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" type="tactic">rewrite</span> <span class="id" type="var">mult_comm</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">mult_assoc</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">mult_assoc</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
现在，是时候讨论下展开和化简了。

<div class="paragraph"> </div>

    你可能已经观察到了像 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>、<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 这样的策略，
    通常总会在需要时自动展开函数的定义。例如，若我们将 <span class="inlinecode"><span class="id" type="var">foo</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 定义为常量 <span class="inlinecode">5</span>... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">foo</span> (<span class="id" type="var">x</span>: <span class="id" type="var">nat</span>) := 5.<br/>
</div>

<div class="doc">
那么在以下证明中 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>（或 <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>，如果我们忽略 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>）
    就会将 <span class="inlinecode"><span class="id" type="var">foo</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 展开为 <span class="inlinecode">(<span class="id" type="keyword">fun</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode">5)</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 并进一步将其化简为 <span class="inlinecode">5</span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fact</span> <span class="id" type="var">silly_fact_1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>, <span class="id" type="var">foo</span> <span class="id" type="var">m</span> + 1 = <span class="id" type="var">foo</span> (<span class="id" type="var">m</span> + 1) + 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
然而，这种自动展开有些保守。例如，若我们用模式匹配定义稍微复杂点的函数... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">bar</span> <span class="id" type="var">x</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">x</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">O</span> ⇒ 5<br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">_</span> ⇒ 5<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
...那么类似的证明就会被卡住： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fact</span> <span class="id" type="var">silly_fact_2_FAILED</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>, <span class="id" type="var">bar</span> <span class="id" type="var">m</span> + 1 = <span class="id" type="var">bar</span> (<span class="id" type="var">m</span> + 1) + 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="comment">(*&nbsp;啥也没做！&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 没有进展的原因在于，它注意到在试着展开 <span class="inlinecode"><span class="id" type="var">bar</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 之后会留下被匹配的
    <span class="inlinecode"><span class="id" type="var">m</span></span>，它是一个变量，因此 <span class="inlinecode"><span class="id" type="keyword">match</span></span> 无法被进一步化简。它还没有聪明到发现
    <span class="inlinecode"><span class="id" type="keyword">match</span></span> 的两个分支是完全相同的。因此它会放弃展开 <span class="inlinecode"><span class="id" type="var">bar</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 并留在那。
    类似地，在试着展开 <span class="inlinecode"><span class="id" type="var">bar</span></span> <span class="inlinecode">(<span class="id" type="var">m</span>+1)</span> 时会留下一个 <span class="inlinecode"><span class="id" type="keyword">match</span></span>，被匹配者是一个函数应用
    （即它本身，即便在展开 <span class="inlinecode">+</span> 的定义后也无法被化简），因此 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 会留下它。 
<div class="paragraph"> </div>

 此时有两种方法可以继续。一种是用 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 将证明分为两种情况，
    每一种都关注于更具体的 <span class="inlinecode"><span class="id" type="var">m</span></span>（<span class="inlinecode"><span class="id" type="var">O</span></span> vs <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">_</span></span>）。在这两种情况下，
    <span class="inlinecode"><span class="id" type="var">bar</span></span> 中的 <span class="inlinecode"><span class="id" type="keyword">match</span></span> 可以继续了，证明则很容易完成。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fact</span> <span class="id" type="var">silly_fact_2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>, <span class="id" type="var">bar</span> <span class="id" type="var">m</span> + 1 = <span class="id" type="var">bar</span> (<span class="id" type="var">m</span> + 1) + 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">m</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
这种方法是可行的，不过它依赖于我们能发现隐藏在 <span class="inlinecode"><span class="id" type="var">bar</span></span> 中的 <span class="inlinecode"><span class="id" type="keyword">match</span></span>
    阻碍了证明的进展。 
<div class="paragraph"> </div>

 一种更直白的方式就是明确地告诉 Coq 去展开 <span class="inlinecode"><span class="id" type="var">bar</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fact</span> <span class="id" type="var">silly_fact_2'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>, <span class="id" type="var">bar</span> <span class="id" type="var">m</span> + 1 = <span class="id" type="var">bar</span> (<span class="id" type="var">m</span> + 1) + 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bar</span>.<br/>
</div>

<div class="doc">
现在很明显，我们在 <span class="inlinecode">=</span> 两边的 <span class="inlinecode"><span class="id" type="keyword">match</span></span> 上都卡住了，不用多想就能用
    <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 来结束证明。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">m</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab155"></a><h1 class="section">对复合表达式使用 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span></h1>

<div class="paragraph"> </div>

 我们已经见过许多通过 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 进行情况分析来处理一些变量的值了。
    不过有时我们需要根据某些<b>表达式</b>的结果的情况来进行推理。我们也可以用
    <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 来做这件事。

<div class="paragraph"> </div>

    下面是一些例子：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">sillyfun</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) : <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? 3 <span class="id" type="keyword">then</span> <span class="id" type="var">false</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? 5 <span class="id" type="keyword">then</span> <span class="id" type="var">false</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">false</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">sillyfun_false</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">sillyfun</span> <span class="id" type="var">n</span> = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">sillyfun</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? 3) <span class="id" type="var">eqn</span>:<span class="id" type="var">E<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;3&nbsp;=&nbsp;true&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;3&nbsp;=&nbsp;false&nbsp;*)</span> <span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? 5) <span class="id" type="var">eqn</span>:<span class="id" type="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;5&nbsp;=&nbsp;true&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;5&nbsp;=&nbsp;false&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
在前面的证明中展开 <span class="inlinecode"><span class="id" type="var">sillyfun</span></span> 后，我们发现卡在
    <span class="inlinecode"><span class="id" type="keyword">if</span></span> <span class="inlinecode">(<span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode">3)</span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode">...</span> 上了。但由于 <span class="inlinecode"><span class="id" type="var">n</span></span> 要么等于 <span class="inlinecode">3</span>
    要么不等于，因此我们可以用 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" type="var">eqb</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">3)</span> 来对这两种情况进行推理。

<div class="paragraph"> </div>

    通常，<span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 策略可用于对任何计算结果进行情况分析。如果 <span class="inlinecode"><span class="id" type="var">e</span></span>
    是某个表达式，其类型为归纳定义的类型 <span class="inlinecode"><span class="id" type="var">T</span></span>，那么对于 <span class="inlinecode"><span class="id" type="var">T</span></span> 的每个构造子
    <span class="inlinecode"><span class="id" type="var">c</span></span>，<span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">e</span></span> 都会生成一个子目标，其中（即目标和上下文中）所有的
    <span class="inlinecode"><span class="id" type="var">e</span></span> 都会被替换成 <span class="inlinecode"><span class="id" type="var">c</span></span>。
<div class="paragraph"> </div>

<a name="lab156"></a><h4 class="section">练习：3 星, standard, optional (combine_split)</h4>
 以下是 <a href="Poly.html"><span class="inlineref">Poly</span></a> 一章中出现过的 <span class="inlinecode"><span class="id" type="tactic">split</span></span> 函数的实现： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">split</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> (<span class="id" type="var">X</span>*<span class="id" type="var">Y</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: (<span class="id" type="var">list</span> <span class="id" type="var">X</span>) * (<span class="id" type="var">list</span> <span class="id" type="var">Y</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [] ⇒ ([], [])<br/>
&nbsp;&nbsp;| (<span class="id" type="var">x</span>, <span class="id" type="var">y</span>) :: <span class="id" type="var">t</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="tactic">split</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">lx</span>, <span class="id" type="var">ly</span>) ⇒ (<span class="id" type="var">x</span> :: <span class="id" type="var">lx</span>, <span class="id" type="var">y</span> :: <span class="id" type="var">ly</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
请证明 <span class="inlinecode"><span class="id" type="tactic">split</span></span> 和 <span class="inlinecode"><span class="id" type="var">combine</span></span> 在以下概念下互为反函数： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">combine_split</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span> <span class="id" type="var">Y</span> (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> (<span class="id" type="var">X</span> * <span class="id" type="var">Y</span>)) <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span> <span class="id" type="var">l</span> = (<span class="id" type="var">l<sub>1</sub></span>, <span class="id" type="var">l<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">combine</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> = <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">eqn</span>:</span> part of the <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> tactic is optional: We've chosen
    to include it most of the time, just for the sake of
    documentation, but many Coq proofs omit it.

<div class="paragraph"> </div>

    When <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>ing compound expressions, however, the information
    recorded by the <span class="inlinecode"><span class="id" type="var">eqn</span>:</span> can actually be critical: if we leave it
    out, then <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> can sometimes erase information we need to
    complete a proof.  例如，假设函数 <span class="inlinecode"><span class="id" type="var">sillyfun1</span></span> 定义如下： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">sillyfun1</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) : <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? 3 <span class="id" type="keyword">then</span> <span class="id" type="var">true</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? 5 <span class="id" type="keyword">then</span> <span class="id" type="var">true</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">false</span>.<br/>
</div>

<div class="doc">
Now suppose that we want to convince Coq of the (rather
    obvious) fact that <span class="inlinecode"><span class="id" type="var">sillyfun1</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> yields <span class="inlinecode"><span class="id" type="var">true</span></span> only when <span class="inlinecode"><span class="id" type="var">n</span></span> is
    odd.  If we start the proof like this (with no <span class="inlinecode"><span class="id" type="var">eqn</span>:</span> on the
    destruct)... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">sillyfun1_odd_FAILED</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">sillyfun1</span> <span class="id" type="var">n</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">oddb</span> <span class="id" type="var">n</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">sillyfun1</span> <span class="id" type="keyword">in</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? 3).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;卡住了...&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
... then we are stuck at this point because the context does
    not contain enough information to prove the goal!  The problem is
    that the substitution performed by <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> is quite brutal &mdash;
    in this case, it thows away every occurrence of <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode">3</span>, but we
    need to keep some memory of this expression and how it was
    destructed, because we need to be able to reason that, since <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span>
    <span class="inlinecode">3</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> in this branch of the case analysis, it must be that <span class="inlinecode"><span class="id" type="var">n</span></span>
    <span class="inlinecode">=</span> <span class="inlinecode">3</span>, from which it follows that <span class="inlinecode"><span class="id" type="var">n</span></span> is odd.

<div class="paragraph"> </div>

    What we want here is to substitute away all existing occurences of
    <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode">3</span>, but at the same time add an equation to the context that
    records which case we are in.  This is precisely what the <span class="inlinecode"><span class="id" type="var">eqn</span>:</span>
    qualifier does. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">sillyfun1_odd</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">sillyfun1</span> <span class="id" type="var">n</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">oddb</span> <span class="id" type="var">n</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">eq</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">sillyfun1</span> <span class="id" type="keyword">in</span> <span class="id" type="var">eq</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? 3) <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqe3</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;现在我们的状态和前面卡住的地方一样了，除了上下文中包含了额外的相等关系假设，<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;它就是我们继续推进所需要的。&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;e<sub>3</sub>&nbsp;=&nbsp;true&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">eqb_true</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Heqe3</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> → <span class="id" type="var">Heqe3</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;e<sub>3</sub>&nbsp;=&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;当我们到达正在推理的函数体中第二个相等关系测试时，我们可以再次使用<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">eqn</span>:</span>，以便结束此证明。&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? 5) <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqe5</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;e<sub>5</sub>&nbsp;=&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">eqb_true</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Heqe5</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> → <span class="id" type="var">Heqe5</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;e<sub>5</sub>&nbsp;=&nbsp;false&nbsp;*)</span> <span class="id" type="tactic">discriminate</span> <span class="id" type="var">eq</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab157"></a><h4 class="section">练习：2 星, standard (destruct_eqn_practice)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">bool_fn_applied_thrice</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> : <span class="id" type="var">bool</span> → <span class="id" type="var">bool</span>) (<span class="id" type="var">b</span> : <span class="id" type="var">bool</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">f</span> (<span class="id" type="var">f</span> (<span class="id" type="var">f</span> <span class="id" type="var">b</span>)) = <span class="id" type="var">f</span> <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab158"></a><h1 class="section">复习</h1>

<div class="paragraph"> </div>

 现在我们已经见过 Coq 中最基础的策略了。未来的章节中我们还会介绍更多，
    之后我们会看到一些更加强大的<b>自动化</b>策略，它能让 Coq 帮我们处理底层的细节。
    不过基本上我们已经有了完成工作所需的东西。

<div class="paragraph"> </div>

    下面是我们已经见过的：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="tactic">intros</span></span>：将前提/变量从证明目标移到上下文中

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>：（当目标形如 <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span> 时）结束证明

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">apply</span></span>：用前提、引理或构造子证明目标

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">apply</span>...</span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>：将前提、引理或构造子应用到上下文中的假设上（正向推理）

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">apply</span>...</span> <span class="inlinecode"><span class="id" type="keyword">with</span>...</span>：为无法被模式匹配确定的变量显式指定值

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>：化简目标中的计算

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>：化简前提中的计算

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>：使用相等关系假设（或引理）来改写目标

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>：使用相等关系假设（或引理）来改写前提

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">symmetry</span></span>：将形如 <span class="inlinecode"><span class="id" type="var">t</span>=<span class="id" type="var">u</span></span> 的目标改为 <span class="inlinecode"><span class="id" type="var">u</span>=<span class="id" type="var">t</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">symmetry</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>：将形如 <span class="inlinecode"><span class="id" type="var">t</span>=<span class="id" type="var">u</span></span> 的前提改为 <span class="inlinecode"><span class="id" type="var">u</span>=<span class="id" type="var">t</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">unfold</span></span>：用目标中的右式替换定义的常量

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">unfold</span>...</span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>：用前提中的右式替换定义的常量

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">destruct</span>...</span> <span class="inlinecode"><span class="id" type="keyword">as</span>...</span>：对归纳定义类型的值进行情况分析

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">destruct</span>...</span> <span class="inlinecode"><span class="id" type="var">eqn</span>:...</span>：为添加到上下文中的等式指定名字，
        记录情况分析的结果

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">induction</span>...</span> <span class="inlinecode"><span class="id" type="keyword">as</span>...</span>: 对归纳定义类型的值进行归纳

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">injection</span></span>: reason by injectivity on equalities
        between values of inductively defined types

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span>: reason by disjointness of constructors on
        equalities between values of inductively defined types

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">assert</span></span> <span class="inlinecode">(<span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">e</span>)</span>（或 <span class="inlinecode"><span class="id" type="tactic">assert</span></span> <span class="inlinecode">(<span class="id" type="var">e</span>)</span> <span class="inlinecode"><span class="id" type="keyword">as</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>）：引入“局部引理”<span class="inlinecode"><span class="id" type="var">e</span></span>
        并称之为 <span class="inlinecode"><span class="id" type="var">H</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">generalize</span></span> <span class="inlinecode"><span class="id" type="tactic">dependent</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>：将变量 <span class="inlinecode"><span class="id" type="var">x</span></span>（以及任何依赖它的东西）
        从上下文中移回目标公式内的前提中 
</li>
</ul>

</div>

<div class="doc">
<a name="lab159"></a><h1 class="section">附加练习</h1>

<div class="paragraph"> </div>

<a name="lab160"></a><h4 class="section">练习：3 星, standard (eqb_sym)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqb_sym</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">n</span> =? <span class="id" type="var">m</span>) = (<span class="id" type="var">m</span> =? <span class="id" type="var">n</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab161"></a><h4 class="section">练习：3 星, advanced, optional (eqb_sym_informal)</h4>
 根据前面你对该引理的形式化证明，给出与它对应的非形式化证明：

<div class="paragraph"> </div>

   定理：对于任何自然数 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>，<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">n</span></span>.

<div class="paragraph"> </div>

   证明： 
</div>
<div class="code code-tight">
&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab162"></a><h4 class="section">练习：3 星, standard, optional (eqb_trans)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqb_trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> =? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">m</span> =? <span class="id" type="var">p</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> =? <span class="id" type="var">p</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab163"></a><h4 class="section">练习：3 星, advanced (split_combine)</h4>
 在前面的练习中，我们证明了对于所有序对的列表，<span class="inlinecode"><span class="id" type="var">combine</span></span> 是 <span class="inlinecode"><span class="id" type="tactic">split</span></span>
    的反函数。你如何形式化陈述 <span class="inlinecode"><span class="id" type="tactic">split</span></span> 是 <span class="inlinecode"><span class="id" type="var">combine</span></span> 的反函数？何时此性质成立？

<div class="paragraph"> </div>

    请完成下面 <span class="inlinecode"><span class="id" type="var">split_combine_statement</span></span> 的定义，其性质指出 <span class="inlinecode"><span class="id" type="tactic">split</span></span>
    是 <span class="inlinecode"><span class="id" type="var">combine</span></span> 的反函数。之后，证明该性质成立。（除必要的 <span class="inlinecode"><span class="id" type="tactic">intros</span></span>
    之外，不要进行更多的 <span class="inlinecode"><span class="id" type="tactic">intros</span></span>，以此来保证你的归纳假设的一般性。
    提示：你需要 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 的什么性质来保证
    <span class="inlinecode"><span class="id" type="tactic">split</span></span> <span class="inlinecode">(<span class="id" type="var">combine</span></span> <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">l<sub>1</sub></span>,<span class="id" type="var">l<sub>2</sub></span>)</span> 成立？） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">split_combine_statement</span> : <span class="id" type="keyword">Prop</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;（“<span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>”&nbsp;表示我们在这里给出了一个逻辑命题。）&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">split_combine</span> : <span class="id" type="var">split_combine_statement</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_split_combine</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab164"></a><h4 class="section">练习：3 星, advanced (filter_exercise)</h4>
 本练习有点难度。为你的归纳假设的形式花点心思。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">filter_exercise</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">test</span> : <span class="id" type="var">X</span> → <span class="id" type="var">bool</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">l</span> <span class="id" type="var">lf</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">filter</span> <span class="id" type="var">test</span> <span class="id" type="var">l</span> = <span class="id" type="var">x</span> :: <span class="id" type="var">lf</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">test</span> <span class="id" type="var">x</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab165"></a><h4 class="section">练习：4 星, advanced, recommended (forall_exists_challenge)</h4>
 定义两个递归的 <span class="inlinecode"><span class="id" type="var">Fixpoints</span></span>，<span class="inlinecode"><span class="id" type="var">forallb</span></span> 和 <span class="inlinecode"><span class="id" type="var">existsb</span></span>。
    第一个检查列表中的每一个元素是否均满足给定的断言：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">forallb</span>&nbsp;<span class="id" type="var">oddb</span>&nbsp;[1;3;5;7;9]&nbsp;=&nbsp;<span class="id" type="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">forallb</span>&nbsp;<span class="id" type="var">negb</span>&nbsp;[<span class="id" type="var">false</span>;<span class="id" type="var">false</span>]&nbsp;=&nbsp;<span class="id" type="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">forallb</span>&nbsp;<span class="id" type="var">evenb</span>&nbsp;[0;2;4;5]&nbsp;=&nbsp;<span class="id" type="var">false</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">forallb</span>&nbsp;(<span class="id" type="var">eqb</span>&nbsp;5)&nbsp;[]&nbsp;=&nbsp;<span class="id" type="var">true</span>
<div class="paragraph"> </div>

</div>
    第二个检查列表中是否存在一个元素满足给定的断言：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">existsb</span>&nbsp;(<span class="id" type="var">eqb</span>&nbsp;5)&nbsp;[0;2;3;6]&nbsp;=&nbsp;<span class="id" type="var">false</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">existsb</span>&nbsp;(<span class="id" type="var">andb</span>&nbsp;<span class="id" type="var">true</span>)&nbsp;[<span class="id" type="var">true</span>;<span class="id" type="var">true</span>;<span class="id" type="var">false</span>]&nbsp;=&nbsp;<span class="id" type="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">existsb</span>&nbsp;<span class="id" type="var">oddb</span>&nbsp;[1;0;0;0;0;3]&nbsp;=&nbsp;<span class="id" type="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">existsb</span>&nbsp;<span class="id" type="var">evenb</span>&nbsp;[]&nbsp;=&nbsp;<span class="id" type="var">false</span>
<div class="paragraph"> </div>

</div>
    接着，用 <span class="inlinecode"><span class="id" type="var">forallb</span></span> 和 <span class="inlinecode"><span class="id" type="var">negb</span></span> 定义一个 <span class="inlinecode"><span class="id" type="var">existsb</span></span> 的非递归版本，名为 <span class="inlinecode"><span class="id" type="var">existsb'</span></span>。

<div class="paragraph"> </div>

    最后，证明定理 <span class="inlinecode"><span class="id" type="var">existsb_existsb'</span></span> 指出 <span class="inlinecode"><span class="id" type="var">existsb'</span></span> 和 <span class="inlinecode"><span class="id" type="var">existsb</span></span> 的行为相同。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">forallb</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">test</span> : <span class="id" type="var">X</span> → <span class="id" type="var">bool</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_forallb_1</span> : <span class="id" type="var">forallb</span> <span class="id" type="var">oddb</span> [1;3;5;7;9] = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_forallb_2</span> : <span class="id" type="var">forallb</span> <span class="id" type="var">negb</span> [<span class="id" type="var">false</span>;<span class="id" type="var">false</span>] = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_forallb_3</span> : <span class="id" type="var">forallb</span> <span class="id" type="var">evenb</span> [0;2;4;5] = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_forallb_4</span> : <span class="id" type="var">forallb</span> (<span class="id" type="var">eqb</span> 5) [] = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">existsb</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">test</span> : <span class="id" type="var">X</span> → <span class="id" type="var">bool</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_existsb_1</span> : <span class="id" type="var">existsb</span> (<span class="id" type="var">eqb</span> 5) [0;2;3;6] = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_existsb_2</span> : <span class="id" type="var">existsb</span> (<span class="id" type="var">andb</span> <span class="id" type="var">true</span>) [<span class="id" type="var">true</span>;<span class="id" type="var">true</span>;<span class="id" type="var">false</span>] = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_existsb_3</span> : <span class="id" type="var">existsb</span> <span class="id" type="var">oddb</span> [1;0;0;0;0;3] = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_existsb_4</span> : <span class="id" type="var">existsb</span> <span class="id" type="var">evenb</span> [] = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">existsb'</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">test</span> : <span class="id" type="var">X</span> → <span class="id" type="var">bool</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">existsb_existsb'</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">test</span> : <span class="id" type="var">X</span> → <span class="id" type="var">bool</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">existsb</span> <span class="id" type="var">test</span> <span class="id" type="var">l</span> = <span class="id" type="var">existsb'</span> <span class="id" type="var">test</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>